FDL - Step of Proof: bool_sq

Step of Proof: bool_sq

Inference at * 1 1 2
Iof proof for Lemma bool sq:

1. x : ?Unit
2. y : ?Unit
3. x = y
4. case x of inl(x) => x | inr(x) => x = case y of inl(x) => x | inr(x) => x
5. case x of inl(x) => True | inr(x) => False = case y of inl(x) => True | inr(x) => False
6.

(True = False)

x ~ y

by ((((((((((D 1)

CollapseTHEN (D 2))

)

CollapseTHEN (AbReduce 4))

)

CollapseTHEN (

CAbReduce 5))

)

CollapseTHEN (Try ((D 6)

CollapseTHEN (Eq))

))

)

CollapseTHEN (

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

C.

Definitions t T, , P Q, A, False, Unit

Lemmas unit wf